\begin{tabbing}
$\forall$$i$, $x$:Id, $T$:Type.
\\[0ex]@$i$: only members of nil affect $x$ :$T$ $\in$ Dsys
\\[0ex]\& (\=$\forall$$D$:Dsys.\+
\\[0ex]@$i$: only members of nil affect $x$ :$T$ $\subseteq$ $D$
\\[0ex]$\Rightarrow$ $D$ realizes ${\it es}$. vartype($i$;$x$) $\subseteq\rho$ $T$ \& $\forall$$e$@$i$. ($x$ after $e$) $=$ ($x$ when $e$) $\in$ $T$)
\-
\end{tabbing}